$\forall$$T$:Type, ${\it eq}$, $r$:($T$$\rightarrow$$T$$\rightarrow\mathbb{B}$).
\\[0ex]($\forall$$a$, $b$:$T$. ($\uparrow$(${\it eq}$($a$,$b$))) $\Leftarrow\!\Rightarrow$ ($a$ = $b$))
\\[0ex]$\Rightarrow$ ($\forall$$x$:$T$, $L$:($T$ List), $z$:$T$. ($z$ $\in$ insert{-}by(${\it eq}$;$r$;$x$;$L$)) $\Leftarrow\!\Rightarrow$ (($z$ = $x$) $\vee$ ($z$ $\in$ $L$)))